Nuprl Lemma : ma-interface-locs_wf 11,40

A:Type, I:MaInterface(A). ma-interface-locs(I (Id List) 
latex


DefinitionsMaInterface(T), ma-interface-locs(I), fpf-domain(f), x.A(x), type List, (x  l), Id, a:A fp B(a), xt(x), hasloc(k;i), x:A  B(x), Type, State(ds), x:AB(x), x:AB(x), left + right, Top, b, Knd, {x:AB(x)} , t  T
Lemmastop wf, decl-state wf, hasloc wf, assert wf, Knd wf, fpf wf, Id wf, l member wf, fpf-trivial-subtype-top, fpf-domain wf

origin